Issue4200.agda:17,5-7
Identifier c₂ is declared erased, so it cannot be used here
when checking that the expression c₂ has type D
